Nuprl Lemma : es_init_wf
11,40
postcript
pdf
es
:event_system{i:l}. es_init(
es
)
i
:Id
es_state(
es
;
i
)
latex
Definitions
x
:
A
.
B
(
x
)
,
Id
,
x
:
A
B
(
x
)
,
event_system{i:l}
,
x
:
A
B
(
x
)
,
es_state(
es
;
i
)
,
es_init(
es
)
,
es_vartype(
es
;
i
;
x
)
,
es-T(
es
)
,
b
,
EState(
T
)
,
t
T
Lemmas
event
system
wf
origin
es:event_system{i:l}. es_init(es) 
i:Id
es_state(es; i) es:event_system{i:l}. es_init(es) i:Ides_state(es; i) x:A. B(x)B(x)
B(x)
b T